STM: increasing implies

STM: increasing implies le

STM: compose increasing

STM: increasing inj

STM: increasing le

STM: increasing is id

STM: increasing lower bound

STM: injection le

STM: disjoint increasing onto

STM: bijection restriction

ABS: primrec(n;b;c)

STM: primrec wf

STM: primrec add

ABS: nondecreasing(f;k)

STM: nondecreasing wf

STM: const nondecreasing

ABS: fadd(f;g)

STM: fadd wf

STM: fadd increasing

ABS: fshift(f;x)

STM: fshift wf

STM: fshift increasing

ABS: finite(T)

STM: finite wf

STM: nsub finite

ABS: f[n:=x]

STM: fappend wf

STM: increasing split

ABS: sum(f(x) | x < k)

STM: sum wf

STM: non neg sum

STM: sum linear

STM: sum scalar mult

STM: sum constant

STM: sum functionality

STM: sum difference

STM: sum le

STM: sum bound

STM: sum lower bound

STM: sum-ite

STM: sum arith1

STM: sum arith

STM: finite-partition

STM: pigeon-hole

STM: isolate summand

STM: empty support

STM: singleton support sum

STM: pair support

STM: sum split

ABS: sum(f(x;y) | x < n; y < m)

STM: double sum wf

STM: pair support double sum

STM: double sum difference

STM: double sum functionality

ABS: R^n

STM: rel exp wf

STM: decidable rel exp

STM: rel exp add

ABS: R1 => R2

STM: rel implies wf

STM: rel exp monotone

ABS: R preserves P

STM: preserved by wf

STM: preserved by monotone

ABS: when P, R1 => R2

STM: cond rel implies wf

STM: cond rel exp monotone

ABS: R^*

STM: rel star wf

STM: rel star monotone

STM: cond rel star monotone

STM: rel star transitivity

STM: rel star monotonic

STM: cond rel star monotonic

STM: preserved by star

STM: rel star closure

STM: rel star closure2

STM: rel star of equiv

STM: cond rel star equiv

STM: rel rel star

STM: rel star trans

STM: rel star weakening

ABS: R^-1

STM: rel inverse wf

STM: rel inverse exp

STM: rel inverse star

STM: rel star symmetric

STM: rel star symmetric 2

STM: preserved by symmetric

ABS: R1  R2

STM: rel or wf

STM: rel implies or left

STM: rel implies or right

STM: symmetric rel or

STM: preserved by or

ABS: P as strong as Q 

STM: as strong wf

STM: as strong transitivity

ABS: f^n

STM: fun exp wf

STM: comb for fun exp wf

STM: fun exp compose

STM: fun exp add

STM: fun exp add1

STM: fun exp add1 sub

STM: iteration terminates

ABS: (i, j)

STM: flip wf

STM: sum switch

STM: flip symmetry

STM: flip bijection

STM: flip inverse

STM: flip twice

ABS: search(k;P)

STM: search wf

STM: search property

STM: search succ

ABS: P  Q

STM: prop and wf

STM: and preserved by

ABS: (ternary) R preserves P 

STM: preserved by2 wf

STM: and preserved by2